|
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics based on the principles of mathematical constructivism. Intuitionistic type theory was introduced by Per Martin-Löf, a Swedish mathematician and philosopher, in 1972. Martin-Löf has modified his proposal a few times; his 1971 impredicative formulation was inconsistent as demonstrated by Girard's paradox. Later formulations were predicative. He proposed both intensional and extensional variants of the theory. For more detail see the section on Martin-Löf type theories below. Intuitionistic type theory is based on a certain analogy or isomorphism between propositions and types: a proposition is identified with the type of its proofs. This identification is usually called the Curry–Howard isomorphism, which was originally formulated for intuitionistic logic and simply typed lambda calculus. Type theory extends this identification to predicate logic by introducing dependent types, that is types which contain values. Type theory internalizes the interpretation of intuitionistic logic proposed by Brouwer, Heyting and Kolmogorov, the so-called BHK interpretation. The types in type theory play a similar role to sets in set theory but functions definable in type theory are always computable. ==Connectives of type theory== In the context of type theory a connective is a way of constructing types, possibly using already given types. The basic connectives of type theory are: 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Intuitionistic type theory」の詳細全文を読む スポンサード リンク
|